M1, M2:MsgA.
M1  M2
 (a:Id, s:M2.state. a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s)) 

latex

Definitions	x:A. B(x), P  Q, unsolvable M.pre(a,s), f(x)?z, t.1, t.2, z != f(x)  P(a;z), t  T, if b then t else f fi , x. t(x), tt, ff, , MsgA, M1  M2, M.state, a declared in M, , Valtype(da;k), A, A c B, P & Q, f  g, x(s), Unit, P  Q, False,
Lemmas	locl wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, Id wf, id-deq wf, ma-state wf, fpf-ap wf, ma-decla wf, ma-st wf, ma-sub wf, msga wf